/*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

#pragma once

/* this file is shared between the kernel and libsel4 */
/*Z 内核将TCB的IPC buffer视作如下结构，用于构建传递消息 */
typedef struct seL4_IPCBuffer_ {
    seL4_MessageInfo_t tag;             /*Z 内核不使用，保留给用户空间 */
    seL4_Word msg[seL4_MsgMaxLength];   /*Z 消息字。对应消息寄存器(用物理寄存器传递)的字，也会保留位置 */
    seL4_Word userData;                 /*Z 手册写用于支持用户库。内核只有IA32用它传递引用能力句柄 */
    seL4_Word caps_or_badges[seL4_MsgMaxExtraCaps]; /*Z 传递的能力(指向sender的CSpace的CSlot索引)，或接收的EP标记 */
    seL4_CPtr receiveCNode;                         /*Z CSlot句柄，指定接收slot所在的CNode */
    seL4_CPtr receiveIndex;                         /*Z            相对上述CNode的CSlot句柄 */
    seL4_Word receiveDepth;                         /*Z            相对上述CNode的位深度(右数位长) */
} seL4_IPCBuffer __attribute__((__aligned__(sizeof(struct seL4_IPCBuffer_))));
/*Z 能力错误类IPC消息的寄存器(IPC buffer)索引 */
enum {
    seL4_CapFault_IP,                       /*Z 发生错误时的指令地址 */
    seL4_CapFault_Addr,                     /*Z 发生错误的CSlot句柄(或地址) */
    seL4_CapFault_InRecvPhase,              /*Z 错误发生在接收信息阶段为1，否则为0 */
    seL4_CapFault_LookupFailureType,        /*Z 能力查找失败原因 */
    seL4_CapFault_BitsLeft,
    seL4_CapFault_DepthMismatch_BitsFound,
    seL4_CapFault_GuardMismatch_GuardFound = seL4_CapFault_DepthMismatch_BitsFound,
    seL4_CapFault_GuardMismatch_BitsFound,
    SEL4_FORCE_LONG_ENUM(seL4_CapFault_Msg),
} seL4_CapFault_Msg;

#define seL4_ReadWrite     seL4_CapRights_new(0, 0, 1, 1)
#define seL4_AllRights     seL4_CapRights_new(1, 1, 1, 1)
#define seL4_CanRead       seL4_CapRights_new(0, 0, 1, 0)
#define seL4_CanWrite      seL4_CapRights_new(0, 0, 0, 1)
#define seL4_CanGrant      seL4_CapRights_new(0, 1, 0, 0)
#define seL4_CanGrantReply seL4_CapRights_new(1, 0, 0, 0)
#define seL4_NoWrite       seL4_CapRights_new(1, 1, 1, 0)
#define seL4_NoRead        seL4_CapRights_new(1, 1, 0, 1)
#define seL4_NoRights      seL4_CapRights_new(0, 0, 0, 0)

